T:Type, l:(T List), x, y, z:T.
no_repeats(T;l)  x before y  l  y before z  l  x before z  l 

latex

ProofTree

Definitions	t  T, x before y  l, P  Q, x:A. B(x), , {T}, P & Q, P  Q, Y, as @ bs, P  Q, P  Q
Lemmas	no repeats wf, sublist wf, sublist transitivity, cons sublist cons, sublist weakening, append overlapping sublists